/*@ i>0 */
int f(int i)
{
  int j;
  j = i+1;
  j = 2*j;
  if (j>2) j = 3;
  else j = 4;
  return j;
}
/*@ result == 3*/
